$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
require 'ext_pr1_v4'

#definieren der nötigen Konstanten:
#sekunden pro minute = 60, minuten pro stunde = 60, Stunden pro Tag = 24
#stunde in sekunden = sekunden pro minute * minuten pro stunde
#tag in sekunden = stunde in sekunden * stunden pro tag

MIN_IN_SEC = 60
HOUR_IN_MIN = 60
DAY_IN_HOUR = 24
HALF_DAY_IN_HOUR = DAY_IN_HOUR/2

HOUR_IN_SEC = MIN_IN_SEC * HOUR_IN_MIN
DAY_IN_SEC = DAY_IN_HOUR * HOUR_IN_SEC
HALF_DAY_IN_SEC = DAY_IN_SEC/2
#arithmetik einer uhr, die mit beliebigen zuständen arbeiten kann
class Object
  def halve?() false end
  def hour24?() false end
  def hour12?() false end
  def min?() false end
  def sec?() false end
  def day_sec?() false end
  def clock?() false end
end

class Integer
  def hour24?() self.int? and self.in?(0...DAY_IN_HOUR) end
  def hour12?() self.int? and self.in?(1..(HALF_DAY_IN_HOUR)) end
  def min?() self.int? and self.in?(0...HOUR_IN_MIN) end
  def sec?() self.int? and self.in?(0...MIN_IN_SEC) end
  def day_sec?() self.int? and self.in?(0...DAY_IN_SEC) end
  
  def normalize() self % DAY_IN_SEC end

  #hilfsfunktion um sekunden in ein array aus hour24, min und sek umzuwandeln
  def hrs_min_sec_from_secs()
  hour = self.divmod(HOUR_IN_SEC)[0]
  min = (self.divmod(HOUR_IN_SEC)[1]).divmod(MIN_IN_SEC)[0]
  sec = (self.divmod(HOUR_IN_SEC)[1]).divmod(MIN_IN_SEC)[1]
  [hour, min, sec]
end

end
class Symbol
  def halve?() self == :AM or self == :PM end
end

###############ClockSec als Klasse##################
#ClockSec ::=  ClockSec[:clock_sec] :: DaySec ::
#0 <= DaySec <= DAY_IN_SEC

def_class(:ClockSec,[:day_sec]) {
def invariant?()
  day_sec.day_sec? end  

#TYPPRÄDIKATE
  def clock?; true end

  
#GLOBALE SELEKTOREN
  #clock_day_sec ::= clock :: (Clock12[halve, hour12, min, sec] | Clock24[hour24, min,sec] | ClockSec[day_sec])::
  # clock -> Int :: (test (clock_day_sec(Clock12[:AM,1,1,1] => 1,
  #clock_sec(Clock24[1,1,1]) => 1, clock_day_sec(ClockSec[3661]) => 1
  #clock_sec(3) => Err, clock_sec("a") => Err)

  def clock_day_sec()
    check_pre(( self.clock?))

    (self.to_clocksec()).day_sec
  end

   # clock_hour24 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour24(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_hour24(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_hour24("a") => Err)

  def clock_hour24()
    check_pre(( self.clock?))
    self.to_clock24().hour24
  end

  #clock_hour12 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour12(Clock12[:AM,1,1,1] => 1,
  #clock_hour12(Clock24[1,1,1]) => 1, clock_hour12(ClockSec[3661]) => 1
  #clock_hour12(3) => Err, clock_hour12("a") => Err)

  def clock_hour12()
    check_pre(( self.clock?))
    self.to_clock12().hour12
  end


  #clock_min ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_min(Clock12[:AM,1,1,1] => 1,
  #clock_min(Clock24[1,1,1]) => 1, clock_min(ClockSec[3661]) => 1
  #clock_min(3) => Err, clock_min("a") => Err)

   def clock_min()
    check_pre(( self.clock?))
    self.to_clock12().min
   end

  #clock_halve ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> :AM|:PM :: (test (clock_halve(Clock12[:AM,1,1,1] => :AM,
  #clock_halve(Clock24[1,1,1]) => :AM, clock_halve(ClockSec[3661]) => :AM
  #clock_halve(3) => Err, clock_halve("a") => Err)

   def clock_halve()
    check_pre((self.clock?))
    self.to_clock12().halve
   end

  # clock_sec ::= clock :: Clock12[halve, hour12, min, sec] || Clock24[hour24, min,sec] || ClockSec[day_sec]::
  # clock -> Int :: (test (clock_sec(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_sec(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_sec("a") => Err)

  def clock_sec()
    check_pre(( self.clock?))
    (self.to_clock24()).sec
  end

#OPERATIONEN
  
#Addieren von zwei Uhrzeiten in sekunden
#clock_sec_add ::sec1, sec2 :: ClockSec[day_sec] x ClockSec[day_sec] => ClockSec[Nat]
#where (sec1 and sec2) >= 0 and (sec1 + sec2) is in (0...DAY_IN_SEC)::
#(test (clock_sec_add(ClockSec[20], ClockSec[50]) => 70,
#clock_sec_add(ClockSec[3000], ClockSec[5600]) => 8600,
#clock_sec_add(ClockSec[30], ClockSec["40"]) => Err,
#clock_sec_add(ClockSec[-10]) => Err)

def clock_sec_add(sec2)
  check_pre((self.clock_sec? and
      sec2.clock_sec?
    ))
  sec = self.day_sec + sec2.day_sec
  ClockSec[sec.normalize()]
end

#Subtrahieren von zwei Uhrzeiten in sekunden
#clock_sec_sub ::= sec1 - sec2 ::  ClockSec[day_sec] x ClockSec[day_sec] => ClockSec[Nat]
# where (day_sec1 and day_sec) >= 0
#(test (clock_sec_sub(ClockSec[90], ClockSec[20] => 70,
#clock_sec_sub(ClockSec[10], ClockSec[20]) => ClockSec[86390],
#clock_sec_sub(ClockSec[30], ClockSec["40"]) => Err,
#clock_sec_sub(ClockSec[-10]) => Err)

def clock_sec_sub(sec2)
  check_pre((self.clock_sec? and sec2.clock_sec?))
 sec = self.day_sec - sec2.day_sec
 
  ClockSec[sec.normalize()]
end

#nachfolger einer uhrzeit, angegeben in sekunden
#clock_sec_succ ::= sec1  ::  ClockSec => ClockSec ::

#clock_sec_succ(ClockSec[86399]) => 0,
#clock_sec_succClockSec[0]) => 1,
#clock_sec_succ(ClockSec["40"]) => Err,


def clock_sec_succ()
 check_pre((self.clock_sec?))
  self.clock_sec_add(ClockSec[1])
end

#vorgänger einer uhrzeit, angegeben in sekunden
#clock_sec_pred ::= sec1  ::  ClockSec[day_sec] => ClockSec[Nat]
# where (sec1 ) >= 0 ::
#(test (clock_sec_pred(ClockSec[90] => 89,
#clock_sec_pred(ClockSec[0]) => 86399,
#clock_sec_pred(ClockSec["40"]) => Err,


def clock_sec_pred() 
  check_pre((self.clock_sec?))
 self.clock_sec_sub(ClockSec[1])
end

#breite Operationen

#ClockSec#clock_add ::= (self, clock) :: ClockSec x (ClockSec|Clock24|Clock12) -> ClockSec
def clock_add(clock2) self.clock_sec_add(clock2.to_clocksec()) end

#ClockSec#clock_sub ::= (self, clock) :: ClockSec x (ClockSec|Clock24|Clock12) -> ClockSec
def clock_sub(clock2) self.clock_sec_sub(clock2.to_clocksec()) end

#ClockSec#clock_succ ::= (self) :: ClockSec -> ClockSec
def clock_succ() self.to_clocksec.clock_sec_succ() end

#ClockSec#clock_pred ::= (self) :: ClockSec -> ClockSec
def clock_pred() self.clock_sec_pred() end

#KONVERSIONEN

#ClockSec zu Clock24 konvertieren
#clocksec_to_clock24  ::= clock :: Clocksec[day_sec] -> Clock24[hour24, min, sec] ::
#test(clocksec_to_clock24(ClockSec[43200]) => Clock24[12, 0, 0],
#clocksec_to_clock24(ClockSec[47593] => Clock24[13, 13, 13],
#clocksec_to_clock24(ClockSec["a"]) => Err)


def clocksec_to_clock24()
  check_pre((self.clock_sec?))
  self.day_sec.hrs_min_sec_from_secs()
  Clock24[self.day_sec.hrs_min_sec_from_secs()[0],self.day_sec.hrs_min_sec_from_secs()[1],self.day_sec.hrs_min_sec_from_secs()[2]]
end

#ClockSec zu Clock12 konvertieren
#clocksec_to_clock12  ::= clock :: Clocksec[day_sec] -> Clock12[halve, hour12, min, sec] ::
#test(clocksec_to_clock12(ClockSec[43200])) => Clock12[:AM,12, 0, 0],
#clocksec_to_clock12(ClockSec[47593]) => Clock12[:PM, 1, 13, 13],
#clocksec_to_clock12(ClockSec["a"]) => Err,



def clocksec_to_clock12()
  check_pre((self.clock_sec?))
  halve = (self.day_sec > HALF_DAY_IN_SEC) ? :PM : :AM
  seconds = halve == :AM ?  self.day_sec : self.day_sec % HALF_DAY_IN_SEC
  Clock12[halve,seconds.hrs_min_sec_from_secs()[0] == 0 ? HALF_DAY_IN_HOUR : seconds.hrs_min_sec_from_secs()[0],seconds.hrs_min_sec_from_secs()[1],seconds.hrs_min_sec_from_secs()[2]]
end


#Konversion in beiebige Uhren
#ClockSec#to_clocksec ::= self :: ClockSec -> ClockSec
def to_clocksec() self end
#ClockSec#to_clock24 ::= self :: ClockSec -> Clock24
def to_clock24() self.clocksec_to_clock24() end
#ClockSec#to_clock12 ::= self :: ClockSec -> Clock12
def to_clock12() self.clocksec_to_clock12() end

#breite Konversion
#ClockSec#to_clock ::= self, value :: (ClockSec x (ClockSec|Clock24|Clock12) -> ClockSec
def to_clock(value) value.to_clocksec() end


    }
   
#Clock24 als Klasse
#Clock24 ::=  Clock24[:hour24, :min, :sec] :: hour24, min, sec ::
#0 <= hour24 <= DAY_IN_HOUR,
#0 <= min <= HOUR_IN_MIN,
#0 <= sec <= MIN_IN_SEC

def_class(:Clock24,[:hour24, :min, :sec]) {
 
  def invariant?()
    #hour24?(hour24)
    hour24.hour24? and
    #min?(min)
    min.min? and
    #sec?(sec)
    sec.sec?
  end 
 
 def clock?; true end 
 
 #GLOBALE SELEKTOREN
 #clock_day_sec ::= clock :: (Clock12[halve, hour12, min, sec] | Clock24[hour24, min,sec] | ClockSec[day_sec])::
  # clock -> Int :: (test (clock_day_sec(Clock12[:AM,1,1,1] => 1,
  #clock_sec(Clock24[1,1,1]) => 1, clock_day_sec(ClockSec[3661]) => 1
  #clock_sec(3) => Err, clock_sec("a") => Err)
  
  def clock_day_sec()
    check_pre(( self.clock?))
    
    (self.to_clocksec()).day_sec
  end
  
   # clock_hour24 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour24(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_hour24(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_hour24("a") => Err)
  
    def clock_hour24()
    check_pre(( self.clock?))
    self.to_clock24().hour24
    end
  
  #clock_hour12 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour12(Clock12[:AM,1,1,1] => 1,
  #clock_hour12(Clock24[1,1,1]) => 1, clock_hour12(ClockSec[3661]) => 1
  #clock_hour12(3) => Err, clock_hour12("a") => Err)
  
      def clock_hour12()
    check_pre(( self.clock?))
    self.to_clock12().hour12
  end
  
      
  #clock_min ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_min(Clock12[:AM,1,1,1] => 1,
  #clock_min(Clock24[1,1,1]) => 1, clock_min(ClockSec[3661]) => 1
  #clock_min(3) => Err, clock_min("a") => Err)
 
   def clock_min()
    check_pre(( self.clock?))
    self.to_clock12().min
  end
  
  #clock_halve ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> :AM|:PM :: (test (clock_halve(Clock12[:AM,1,1,1] => :AM,
  #clock_halve(Clock24[1,1,1]) => :AM, clock_halve(ClockSec[3661]) => :AM
  #clock_halve(3) => Err, clock_halve("a") => Err)
  
      def clock_halve()
    check_pre((self.clock?))
    self.to_clock12().halve
    
  end

  # clock_sec ::= clock :: Clock12[halve, hour12, min, sec] || Clock24[hour24, min,sec] || ClockSec[day_sec]::
  # clock -> Int :: (test (clock_sec(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_sec(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_sec("a") => Err)
  
  def clock_sec()
    check_pre(( self.clock?))
    (self.to_clock24()).sec
  end
  
#Clock24 auf ClockSec konvertieren
#clock24_to_clocksec ::= clock :: Clock24[hour24, min, sec] => ClockSec[day_sec] ::
#test(clock_24_to_clocksec(Clock24[0, 0, 0]) => ClockSec[0],
#clock_24_to_clocksec(Clock24[10, 10, 10]) => ClockSec[36610],
#clock_24_to_clocksec(Clock24[0, 0, "a"]) => Err,
#clock_24_to_clocksec(Clock24[-1, 0, 0]) => Err)
  def clock24_to_clocksec()
  check_pre((self.clock24?))
    ClockSec[(self.hour24 * HOUR_IN_SEC) + (self.min * MIN_IN_SEC) + self.sec]
    
end

#Clock24 zu Clock12 konvertieren
#clock24_to_clock12 ::= clock :: Clock24[hour24, min, sec] -> Clock12[halve, hour12, min, sec] ::
#test (clock24_to_clock12(clock24[11,11,11])) => Clock12[:AM,11,11,11],
#(clock24_to_clock12(Clock24[13,13,13])) => Clock12[:PM,1,13,13],
#(clock24_to_clock12(Clock24[1,1,-1]) => Err,

def clock24_to_clock12()
  check_pre((self.clock24?))
(self.clock24_to_clocksec()).clocksec_to_clock12()
end

#Konvertierung allgemein
#Clock24#to_clocksec ::= self :: Clock24 -> ClockSec
def to_clocksec() self.clock24_to_clocksec() end
#Clock24#to_clocksec ::= self :: Clock24 -> Clock24
def to_clock24() self end
#Clock24#to_clocksec ::= self :: Clock24 -> Clock12
def to_clock12() self.clock24_to_clock12() end
#Clock24#to_clock ::= self, value :: Clock24 x (ClockSec|Clock24|Clock12) ->  Clock24
def to_clock(value) value.to_clock24() end

#Clock24#clock_add ::= (self, clock) :: Clock24 x (ClockSec|Clock24|Clock12) -> Clock24
def clock_add(clock2) self.to_clock((self.to_clocksec()).clock_sec_add(clock2.to_clocksec())) end

#Clock24#clock_sub ::= (self, clock) :: Clock24 x (ClockSec|Clock24|Clock12) -> Clock24
def clock_sub(clock2) self.to_clock((self.to_clocksec()).clock_sec_sub(clock2.to_clocksec())) end

#Clock24#clock_succ ::= (self) :: Clock24 -> Clock24
def clock_succ() (self.to_clocksec.clock_sec_succ()).to_clock24() end

#Clock24#clock_pred ::= (self) :: Clock24 -> Clock24
def clock_pred() (self.to_clocksec.clock_sec_pred()).to_clock24() end
    }

#Clock12 als Klasse
#Clock12 ::= Clock12[:halve, :hour12, :min, :sec] :: halve, hour, min, sec ::
#halve = (:AM or :PM),
#0 <= hour12 <= (HALF_DAY_IN_HOUR),
#0 <= min <= HOUR_IN_MIN,
#0 <= sec <= MIN_IN_SEC

def_class(:Clock12,[:halve, :hour12, :min, :sec]) {
  def invariant?()
    halve.halve? and
    hour12.hour12? and
    min.min? and
    sec.sec?
  end
  
  #GLOBALE SELEKTOREN
  #clock_day_sec ::= clock :: (Clock12[halve, hour12, min, sec] | Clock24[hour24, min,sec] | ClockSec[day_sec])::
  # clock -> Int :: (test (clock_day_sec(Clock12[:AM,1,1,1] => 1,
  #clock_sec(Clock24[1,1,1]) => 1, clock_day_sec(ClockSec[3661]) => 1
  #clock_sec(3) => Err, clock_sec("a") => Err)
  
  def clock_day_sec()
    check_pre((self.clock?))
    
    (self.to_clocksec()).day_sec
  end
  
   # clock_hour24 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour24(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_hour24(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_hour24("a") => Err)
  
    def clock_hour24()
    check_pre(( self.clock?))
    self.to_clock24().hour24
    end
  
  #clock_hour12 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_hour12(Clock12[:AM,1,1,1] => 1,
  #clock_hour12(Clock24[1,1,1]) => 1, clock_hour12(ClockSec[3661]) => 1
  #clock_hour12(3) => Err, clock_hour12("a") => Err)
  
      def clock_hour12()
    check_pre(( self.clock?))
    self.to_clock12().hour12
  end
  
      
  #clock_min ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> Int :: (test (clock_min(Clock12[:AM,1,1,1] => 1,
  #clock_min(Clock24[1,1,1]) => 1, clock_min(ClockSec[3661]) => 1
  #clock_min(3) => Err, clock_min("a") => Err)
 
   def clock_min()
    check_pre(( self.clock?))
    self.to_clock12().min
  end
  
  #clock_halve ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
  # clock -> :AM|:PM :: (test (clock_halve(Clock12[:AM,1,1,1] => :AM,
  #clock_halve(Clock24[1,1,1]) => :AM, clock_halve(ClockSec[3661]) => :AM
  #clock_halve(3) => Err, clock_halve("a") => Err)
  
      def clock_halve()
    check_pre((self.clock?))
    self.to_clock12().halve
    
  end

  # clock_sec ::= clock :: Clock12[halve, hour12, min, sec] || Clock24[hour24, min,sec] || ClockSec[day_sec]::
  # clock -> Int :: (test (clock_sec(Clock12[:AM,1,1,1] => 1,
  #clock_hour24(Clock24[1,1,1]) => 1, clock_sec(ClockSec[3661]) => 1
  #clock_hour24(3) => Err, clock_sec("a") => Err)
  
  def clock_sec()
    check_pre(( self.clock?))
    (self.to_clock24()).sec
  end
  
  def clock?; true end
#Clock12 auf ClockSec konvertieren
#clock12_to_clocksec ::= clock :: Clock12[halve, hour12, min, sec] => ClockSec[day_sec] ::
#test
#(clock_12_to_clocksec(Clock12[:AM, 12, 0, 0]) => ClockSec[0], 
#clock_12_to_clocksec(Clock12[:PM, 12, 0, 0]) => ClockSec[43200],
#clock_12_to_clocksec(Clock12[0, 0, "a"]) => Err,)

def clock12_to_clocksec()
  check_pre((self.clock12?))
  sec = (((self.halve == :AM ? 0 : 12) * HOUR_IN_SEC) +
      ((self.hour12 == 12) ? 0 : (self.hour12 * HOUR_IN_SEC)) + 
      (self.min * MIN_IN_SEC) + self.sec)
    ClockSec[sec.normalize()]
end

#Clock12 zu Clock24 konvertieren
#clock12_to_clock24 ::= clock :: Clock12[halve, hour12, min, sec] -> Clock24[hour24, min, sec] ::
#test (clock12_to_clock24(Clock12[:AM,11,11,11]) => Clock24[11,11,11]),
#(clock12_to_clock24(Clock12[:PM,1,13,13]) => Clock24[13,13,13],
#(clock24_to_clock12(Clock12[:AM,1,1,-1]) => Err)

def clock12_to_clock24()
  check_pre((self.clock12?))
  (self.clock12_to_clocksec()).clocksec_to_clock24()
end

#Konvertierung allgemein

#Clock12#to_clocksec ::= self :: Clock12 -> ClockSec
def to_clocksec() self.clock12_to_clocksec() end
#Clock12#to_clock24 ::= self :: Clock12 -> Clock24
def to_clock24() self.clock12_to_clock24 end
#Clock12#to_clock12 ::= self :: Clock12 -> Clock12
def to_clock12()  self end


def to_clock(value) value.to_clock12() end

#Clock12#clock_add ::= (self, clock) :: Clock12 x (ClockSec|Clock24|Clock12) -> Clock12
def clock_add(clock2) self.to_clock((self.to_clocksec()).clock_sec_add(clock2.to_clocksec())) end

#Clock12#clock_sub ::= (self, clock) :: Clock12 x (ClockSec|Clock24|Clock12) -> Clock12
def clock_sub(clock2) self.to_clock((self.to_clocksec()).clock_sec_sub(clock2.to_clocksec())) end

#Clock12#clock_succ ::= (self) :: Clock12 -> Clock12
def clock_succ() (self.to_clocksec.clock_sec_succ()).to_clock12() end

#Clock12#clock_pred ::= (self) :: Clock12 -> Clock12
def clock_pred() (self.to_clocksec.clock_sec_pred()).to_clock12() end
    
}



#to_clock24
#Konvertierung in eine 24 stunden-Uhr
#to_clock24 ::= clock :: Clock12 or ClockSec 
#-> Clock24[hour24, min, sec]
#test (to_clock24(ClockSec[43200]) => Clock24[12, 0, 0],
#to_clock24(ClockSec[47593] => Clock24[13, 13, 13], 
#(to_clock24(Clock12[:AM,11,11,11]) => Clock24[11,11,11]),
#(to_clock24(Clock12[:PM,1,13,13]) => Clock24[13,13,13],
#to_clock24(200) => Err,
#to_clock24("a") => Err



#to_clock12
#Konvertierung in eine 12 stunden uhr
#to_clock12 ::= clock :: Clock24[hour24, min, sec] or ClockSec[day_sec]
#-> Clock12[halve, hour12, min, sec]
#test(to_clock12((ClockSec[43200])) => Clock12[:AM,12, 0, 0],
#(to_clock12(ClockSec[47593])) => Clock12[:PM, 1, 13, 13],
#(to_clock12(clock24[11,11,11])) => Clock12[:AM,11,11,11],
#(to_clock12(Clock24[13,13,13])) => Clock12[:PM,1,13,13],
#to_clock24(200) => Err,
#to_clock24("a") => Err


#to_clock
#beliebige konversion von uhren
#to_clock ::= clock1, clock2 :: Clock x Clock -> Clock ::
#test(to_clock(Clock24[6,6,6], ClockSec[43200]) => Clock24[12,0,0],
#to_clock(Clock24[12,3,1], Clock12[:PM,12,0,0]) => Clock24[12,0,0],
#to_clock(ClockSec[10000], Clock12[:AM, 12,12,12]) => ClockSec[732],
#to_clock(ClockSec[10000], Clock24[12,0,0]) => ClockSec[43200],
#to_clock(Clock12[:PM, 1,1,1], clock24[0,0,0]) => Clock12[:AM, 12,0,0]
#to_clock(Clock12[:PM,1,1,1], clocksec[0]) => Clock12[:AM, 12,0,0]
#to_clock("a". Clock12[:AM, 12,0,0]) => Err)


  
  #clock_add
  #Addieren von zwei Uhrzeiten
  #clock_add ::= clock1, clock2 :: Clock x Clock => Clock ::
  #test(clock_add(ClockSec[3000], ClockSec[5600])) => ClockSec[8600]
  #(clock_add(Clocksec[3000], Clock24[1,1,1])) => ClockSec[6661]
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,1])) => ClockSec[6661]
  #(clock_add(Clock12[:AM,1,1,1], ClockSec[1000])) => Clock12[:AM,1,17,41]
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1])) => Clock12[:AM,2,2,2]
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,1])) => Clock12[:AM,2,2,2]
  #(clock_add(Clock24[1,1,1], ClockSec[1000])) => Clock24[1,17,17]
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,1])) => Clock24[2,2,2]
  #(clock_add(Clock24[1,1,1], Clock24[1,1,1])) => Clock24[2,2,2]
  #exc
  #clock_add(ClockSec["a], ClockSec[5600])) => Err
  #clock_add(ClockSec[3000], ClockSec["a"])) => Err
  #clock_add(ClockSec[-1], ClockSec[5600])) => Err
  #clock_add(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_add(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_add(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_add(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_add(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_add(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_add(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_add(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_add(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_add(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_add(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_add(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_add(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_add(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_add(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_add(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_add(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  

  #clock_sub
  #Subtrahieren von zwei Uhrzeiten
  #clock_sub ::= clock1, clock2 :: Clock x Clock => Clock ::
  #test(clock_sub(ClockSec[83800], ClockSec[5600])) => ClockSec[8600]
  #(clock_sub(Clocksec[85739], Clock24[1,1,1])) => ClockSec[6661]
  #(clock_sub(Clocksec[85739], Clock12[:AM,1,1,1])) => ClockSec[6661]
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec[1000])) => Clock12[:PM,12,44,45]
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1])) => Clock12[:AM,12,0,0]
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,1])) => Clock12[:AM,12,0,0]
  #(clock_sub(Clock24[1,1,1], ClockSec[1000])) => Clock24[0,44,45]
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,1])) => Clock24[2,2,2]
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,1])) => Clock24[2,2,2]
  #exc
  #clock_sub(ClockSec["a"], ClockSec[5600])) => Err
  #clock_sub(ClockSec[3000], ClockSec["a"])) => Err
  #clock_sub(ClockSec[-1], ClockSec[5600])) => Err
  #clock_sub(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_sub(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_sub(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_sub(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_sub(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_sub(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_sub(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_sub(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_sub(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_sub(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_sub(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_sub(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
#  def clock_sub(clock1,clock2)
#     check_pre(( clock?(clock1) and (clock?(clock2)) ))
#
#    to_clock(clock1, (clock_sec_sub(to_clocksec(clock1), to_clocksec(clock2))))
#  end
  
  
  #clock_succ
  #Nachfolger einer Uhrzeit
  #clock_succ ::= clock1,clock2 :: Clock x Clock => Clock :: 
  #test(clock_succ(ClockSec[1], ClockSec[1]) => Clock24[2]
  #(clock_succ(ClockSec[1], Clock12[:AM,1,1,1]) => ClockSec[3662]
  #(clock_succ(ClockSec[1], Clock24[1,1,1] => [3662]
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec[1]) => Clock12[:AM,1,1,2]
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1]) => Clock12[:AM,1,1,2]
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,1] => Clock12[:AM,1,1,2]
  #(clock_succ(Clock24[1,1,1], ClockSec[1]) => Clock24[1,1,2]
  #(clock_succ(Clock24[1,1,1]), Clock12[:AM,1,1,1] => Clock24[1,1,2]
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,1]) => Clock24[1,1,2]
  #exc
  #clock_succ(ClockSec["a"], ClockSec[5600])) => Err
  #clock_succ(ClockSec[3000], ClockSec["a"])) => Err
  #clock_succ(ClockSec[-1], ClockSec[5600])) => Err
  #clock_succ(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_succ(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_succ(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_succ(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_succ(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_succ(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_succ(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_succ(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_succ(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_succ(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_succ(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_succ(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
#  def clock_succ(clock1,clock2)
#     check_pre(( clock?(clock1) and (clock?(clock2)) ))
#    
#  to_clock(clock1, (clock_sec_succ(to_clocksec(clock2))))
#  end
  
  #clock_pred
  #Vorgänger einer Uhrzeit
  #clock_pred ::= clock1,clock2 :: Clock x Clock => Clock :: 
  #test(clock_pred(ClockSec[2], ClockSec[1]) => Clock24[0]
  #(clock_pred(ClockSec[1], Clock12[:AM,1,1,1]) => ClockSec[3660]
  #(clock_pred(ClockSec[1], Clock24[1,1,1] => [3660]
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec[1]) => Clock12[:AM,1,1,0]
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,1]) => Clock12[:AM,1,1,0]
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,1] => Clock12[:AM,1,1,0]
  #(clock_pred(Clock24[1,1,1], ClockSec[1]) => Clock24[1,1,0]
  #(clock_pred(Clock24[1,1,1]), Clock12[:AM,1,1,1] => Clock24[1,1,0]
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,1]) => Clock24[1,1,0]
  #exc
  #clock_pred(ClockSec["a"], ClockSec[5600])) => Err
  #clock_pred(ClockSec[3000], ClockSec["a"])) => Err
  #clock_pred(ClockSec[-1], ClockSec[5600])) => Err
  #clock_pred(ClockSec[3000], ClockSec[-1])) => Err
  #(clock_pred(Clocksec["a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24["a",1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,"a",1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clocksec[-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[-1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,-1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock24[1,1,-1])) => Err
  #(clock_pred(Clocksec["a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clocksec[-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clocksec[3000], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec["a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], ClockSec[1000])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], ClockSec[-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock12["a",1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,"a",1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,"a",1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24["a",1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,"a",1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clock12[:AM,-1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,-1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[-1,1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,-1,1])) => Err
  #(clock_pred(Clock12[:AM,1,1,1], Clock24[1,1,-1])) => Err
  #(clock_pred(Clock24["a",1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,"a",1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,"a"], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,1], ClockSec["a"])) => Err
  #(clock_pred(Clock24[-1,1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,-1,1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,-1], ClockSec[1000])) => Err
  #(clock_pred(Clock24[1,1,1], ClockSec[-1000])) => Err
  #(clock_pred(Clock24["a",1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,"a",1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,"a"], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12["a",1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,"a",1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,"a",1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,1,"a"])) => Err
  #(clock_pred(Clock24[-1,1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,-1,1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,-1], Clock12[:AM,1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,-1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,-1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock12[:AM,1,1,-1])) => Err
  #(clock_pred(Clock24["a",1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,"a",1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,"a"], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24["a",1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,"a",1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,"a"])) => Err
  #(clock_pred(Clock24[-1,1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,-1,1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,-1], Clock24[1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[-1,1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,-1,1])) => Err
  #(clock_pred(Clock24[1,1,1], Clock24[1,1,-1])) => Err
  
#  def clock_pred(clock1,clock2)
#     check_pre(( clock?(clock1) and (clock?(clock2)) ))
#    
#  to_clock(clock1, (clock_sec_pred(to_clocksec(clock2))))
#  end
  
#  #allgemeine selektoren
#  
#  #clock_sec ::= clock :: (Clock12[halve, hour12, min, sec] | Clock24[hour24, min,sec] | ClockSec[day_sec])::
#  # clock -> Int :: (test (clock_day_sec(Clock12[:AM,1,1,1] => 1,
#  #clock_sec(Clock24[1,1,1]) => 1, clock_day_sec(ClockSec[3661]) => 1
#  #clock_sec(3) => Err, clock_sec("a") => Err)
#  
#  def clock_day_sec()
#    check_pre(( self.clock?))
#    
#    (self.to_clocksec()).day_sec
#  end
#  
#    #clock_hour24 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
#  # clock -> Int :: (test (clock_hour24(Clock12[:AM,1,1,1] => 1,
#  #clock_hour24(Clock24[1,1,1]) => 1, clock_hour24(ClockSec[3661]) => 1
#  #clock_hour24(3) => Err, clock_hour24("a") => Err)
#  
#    def clock_hour24()
#    check_pre(( self.clock?))
#    self.to_clock24().hour24
#    end
#  
#  #clock_hour12 ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
#  # clock -> Int :: (test (clock_hour12(Clock12[:AM,1,1,1] => 1,
#  #clock_hour12(Clock24[1,1,1]) => 1, clock_hour12(ClockSec[3661]) => 1
#  #clock_hour12(3) => Err, clock_hour12("a") => Err)
#  
#      def clock_hour12()
#    check_pre(( self.clock?))
#    self.to_clock12().hour12
#  end
#  
#      
#  #clock_min ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
#  # clock -> Int :: (test (clock_min(Clock12[:AM,1,1,1] => 1,
#  #clock_min(Clock24[1,1,1]) => 1, clock_min(ClockSec[3661]) => 1
#  #clock_min(3) => Err, clock_min("a") => Err)
# 
#   def clock_min()
#    check_pre(( self.clock?))
#    self.to_clock12().min
#  end
#  
#  #clock_halve ::= clock :: Clock12[halve, hour12, min, sec] or Clock24[hour24, min,sec] ClockSec[day_sec]::
#  # clock -> :AM|:PM :: (test (clock_halve(Clock12[:AM,1,1,1] => :AM,
#  #clock_halve(Clock24[1,1,1]) => :AM, clock_halve(ClockSec[3661]) => :AM
#  #clock_halve(3) => Err, clock_halve("a") => Err)
#  
#      def clock_halve()
#    check_pre((self.clock?))
#    self.to_clock12().halve
#    
#  end
